T:Type, L1, L2:T List, i, j:||L1||.
L2 = swap(L1;i;j)
 {L2[i] = L1[j]  T & L2[j] = L1[i]  T & ||L2|| = ||L1||   & L1 = swap(L2;i;j)
 {& (x:||L2||. x = i    x = j    L2[x] = L1[x]  T)} 

latex

Definitions	t  T, x:A. B(x), ||as||, {i..j}, swap(L;i;j), Prop, P & Q, {T}, P  Q, False, A, AB, i  j < k, b, b, , i=j, P  Q, Unit, ij, (i, j), l[i], P  Q, SQType(T)
Lemmas	swap swap, swap length, bool wf, swap select, le wf, select wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bnot wf, not wf, assert wf, swap wf, int seg wf, length wf1